MAYBE 20.191 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could not be shown:



HASKELL
  ↳ LR

mainModule List
  ((intersect :: [Float ->  [Float ->  [Float]) :: [Float ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (\vv2 ->
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []
) xs


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\vv2
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []

is transformed to
intersectBy0 eq ys vv2 = 
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((intersect :: [Float ->  [Float ->  [Float]) :: [Float ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []

is transformed to
intersectBy00 eq ys x = if any (eq xys then x : [] else []
intersectBy00 eq ys _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((intersect :: [Float ->  [Float ->  [Float]) :: [Float ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x  if any (eq x) ys then x : [] else []
intersectBy00 eq ys _ []


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if any (eq xys then x : [] else []

is transformed to
intersectBy000 x True = x : []
intersectBy000 x False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((intersect :: [Float ->  [Float ->  [Float]) :: [Float ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys _ []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((intersect :: [Float ->  [Float ->  [Float]) :: [Float ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ Narrow
                      ↳ Narrow

mainModule List
  (intersect :: [Float ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pePe(Succ(wv32700), Succ(wv33200), wv326) → new_pePe(wv32700, wv33200, wv326)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wv8200), Succ(wv400000)) → new_primPlusNat(wv8200, wv400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(wv300000), wv40000) → new_primMulNat(wv300000, wv40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_foldr(wv60, wv6100, :(wv650, wv651)) → new_foldr(wv60, wv6100, wv651)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ DependencyGraphProof
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0008(wv74, wv7500, wv77, Zero, wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) → new_intersectBy0000(wv74, wv750, wv95, wv780, wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00023(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00048(wv173, wv41) → new_intersectBy00088(wv41)
new_intersectBy00085(Neg(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00070(wv41)
new_intersectBy000122(wv74, Succ(wv7500), wv77, Zero, wv79) → new_intersectBy0008(wv74, wv7500, wv77, Zero, wv79)
new_intersectBy00052(wv30100000, Succ(wv1950), wv41) → new_intersectBy00089(wv30100000, wv41)
new_intersectBy00078(wv285, wv41) → new_intersectBy000111(wv41)
new_intersectBy00023(wv30000, wv30100000, Succ(wv990), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy00098(wv34, wv3500, Succ(wv1900), wv39) → new_intersectBy0009(wv34, Succ(wv3500), wv39)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00046(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Zero, Neg(Succ(wv3800)), wv39) → new_intersectBy00097(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00071(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00065(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00037(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00027(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00037(wv30100000, Succ(wv1390), wv41) → new_intersectBy00089(wv30100000, wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00069(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00073(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00046(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00054(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00085(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00078(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0005(wv74, wv750, :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00030(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00068(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00067(wv30100000, Succ(wv2510), wv41) → new_intersectBy000112(wv30100000, wv41)
new_intersectBy0004(wv74, wv7500, Zero, Succ(Succ(wv10800)), wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00041(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00029(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00033(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy00039(wv147, wv41) → new_intersectBy00091(wv41)
new_intersectBy00083(Succ(wv3120), wv41) → new_intersectBy000113(wv41)
new_intersectBy000116(wv47, wv4800, wv2600, Succ(wv2940), wv52) → new_intersectBy000108(wv47, wv4800, wv2600, wv2940, wv52)
new_intersectBy00071(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00064(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00060(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000121(wv74, wv750, wv77, wv780, :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy00085(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00079(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00031(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00059(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00059(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00025(wv30000, new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00057(wv30100000, Succ(wv2120), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Succ(wv2600), Neg(Zero), wv52) → new_intersectBy000116(wv47, wv4800, wv2600, Zero, wv52)
new_intersectBy00064(wv30100000, Succ(wv2300), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy000103(wv60, wv6100, Zero, Succ(Succ(wv23800)), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy0004(wv74, wv7500, wv77, Zero, wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy000107(wv60, wv6100, Succ(wv2420), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy000102(wv60, wv2040, wv65) → new_intersectBy000101(wv60, Zero, wv65)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Zero, Neg(Zero), wv52) → new_intersectBy000119(wv47, wv4800, Zero, wv52)
new_intersectBy00030(wv30100000, Succ(wv1210), wv41) → new_intersectBy00086(wv30100000, wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00036(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00099(wv34, wv3500, Succ(wv1920), wv39) → new_intersectBy0009(wv34, Succ(wv3500), wv39)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00070(wv41)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Zero, Neg(Zero), wv39) → new_intersectBy00097(wv34, wv3500, Zero, wv39)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00076(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00020(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00042(wv34, Pos(wv350), Succ(wv1480), Pos(wv380), wv39) → new_intersectBy0005(wv34, wv350, wv39)
new_intersectBy00055(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00043(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Zero, Pos(Succ(wv5100)), wv52) → new_intersectBy000118(wv47, wv4800, new_primPlusNat0(new_primMulNat0(wv4800, wv5100), Succ(wv5100)), wv52)
new_intersectBy00071(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00067(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00033(wv41)
new_intersectBy00095(wv34, wv1480, wv39) → new_intersectBy0009(wv34, Zero, wv39)
new_intersectBy00020(wv30000, Succ(wv910), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), wv301), Float(Pos(Succ(wv40000)), wv401), wv41) → new_intersectBy000(wv30000, wv301, new_primMulNat0(wv30000, wv40000), wv40000, wv401, wv41)
new_intersectBy000109(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00061(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Pos(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00033(wv41)
new_intersectBy00071(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00057(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00027(wv30100000, Succ(wv1120), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00019(wv30000, wv30100000, Succ(wv860), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00049(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Succ(wv2600), Neg(Succ(wv5100)), wv52) → new_intersectBy000116(wv47, wv4800, wv2600, new_primPlusNat0(new_primMulNat0(wv4800, wv5100), Succ(wv5100)), wv52)
new_intersectBy00072(wv47, Neg(Zero), Succ(wv2600), Neg(Succ(wv5100)), wv52) → new_intersectBy000104(wv47, Zero, wv52)
new_intersectBy00026(wv30000, :(wv410, wv411)) → new_intersectBy00022(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy00090(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00071(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00068(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000110(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00062(wv229, wv41) → new_intersectBy000111(wv41)
new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) → new_intersectBy0002(wv74, wv750, wv97, wv780, wv79)
new_intersectBy00041(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00039(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), wv301), Float(Pos(Zero), wv401), wv41) → new_intersectBy00041(wv301, wv401, wv41)
new_intersectBy00071(Pos(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy000(wv74, Neg(wv750), Succ(wv760), wv77, Neg(wv780), wv79) → new_intersectBy0003(wv74, wv750, new_primPlusNat0(wv760, wv77), wv780, wv79)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Zero, Neg(Zero), wv65) → new_intersectBy000107(wv60, wv6100, Zero, wv65)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Zero, Pos(Zero), wv39) → new_intersectBy00096(wv34, wv3500, Zero, wv39)
new_intersectBy000105(wv60, wv2040, wv65) → new_intersectBy000104(wv60, Zero, wv65)
new_intersectBy00041(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00028(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00012(wv74, wv7500, Succ(wv770), Succ(wv10800), wv79) → new_intersectBy00012(wv74, wv7500, wv770, wv10800, wv79)
new_intersectBy00085(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00070(wv41)
new_intersectBy00085(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00080(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00018(wv30000, :(wv410, wv411)) → new_intersectBy00013(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00070(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00070(wv41)
new_intersectBy00082(wv30100000, Succ(wv3070), wv41) → new_intersectBy000112(wv30100000, wv41)
new_intersectBy00041(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00036(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00039(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00072(wv47, Pos(Zero), Succ(wv2600), Pos(Zero), wv52) → new_intersectBy000115(wv47, wv2600, wv52)
new_intersectBy0007(Float(Pos(Succ(wv30000)), wv301), Float(Neg(Succ(wv40000)), wv401), wv41) → new_intersectBy00042(wv30000, wv301, new_primPlusNat0(new_primMulNat0(wv30000, wv40000), Succ(wv40000)), wv401, wv41)
new_intersectBy000100(wv74, wv7500, Succ(wv770), Succ(wv11000), wv79) → new_intersectBy000100(wv74, wv7500, wv770, wv11000, wv79)
new_intersectBy00011(wv74, Succ(wv7500), wv77, Zero, wv79) → new_intersectBy0004(wv74, wv7500, wv77, Zero, wv79)
new_intersectBy00077(Succ(wv2820), wv41) → new_intersectBy000110(wv41)
new_intersectBy00055(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00054(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00017(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00070(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy000(wv74, Pos(wv750), Succ(wv760), wv77, Pos(wv780), wv79) → new_intersectBy0000(wv74, wv750, new_primPlusNat0(wv760, wv77), wv780, wv79)
new_intersectBy00015(wv30000, Succ(wv3200), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy00072(wv47, Pos(wv480), Succ(wv2600), Neg(wv510), wv52) → new_intersectBy000101(wv47, wv480, wv52)
new_intersectBy00085(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00081(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy00013(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy00074(Succ(wv2730), wv41) → new_intersectBy000110(wv41)
new_intersectBy00055(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00049(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00019(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000117(wv47, wv2600, wv52) → new_intersectBy000104(wv47, Zero, wv52)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00044(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000116(wv47, wv4800, wv2600, Zero, wv52) → new_intersectBy000104(wv47, Succ(wv4800), wv52)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00051(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00094(wv34, wv3500, wv1480, Zero, wv39) → new_intersectBy0009(wv34, Succ(wv3500), wv39)
new_intersectBy00051(wv194, wv41) → new_intersectBy00091(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00064(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00029(wv120, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00017(wv30000, Succ(wv830), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00052(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Zero, Pos(Succ(wv6400)), wv65) → new_intersectBy000106(wv60, wv6100, new_primPlusNat0(new_primMulNat0(wv6100, wv6400), Succ(wv6400)), wv65)
new_intersectBy00053(Succ(wv2000), wv41) → new_intersectBy00090(wv41)
new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) → new_intersectBy0001(wv74, wv750, wv96, wv780, wv79)
new_intersectBy00011(wv74, Zero, wv77, Succ(wv7800), wv79) → new_intersectBy0005(wv74, Zero, wv79)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00079(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000112(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00085(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00063(wv41)
new_intersectBy000(wv74, Pos(Succ(wv7500)), Zero, wv77, Pos(Zero), wv79) → new_intersectBy0004(wv74, wv7500, wv77, Zero, wv79)
new_intersectBy0006(wv74, wv77, wv79) → new_intersectBy0005(wv74, Zero, wv79)
new_intersectBy00071(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00069(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Succ(wv2040), Pos(Succ(wv6400)), wv65) → new_intersectBy000103(wv60, wv6100, wv2040, new_primPlusNat0(new_primMulNat0(wv6100, wv6400), Succ(wv6400)), wv65)
new_intersectBy00085(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00074(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00058(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0004(wv74, wv7500, Succ(wv770), Succ(Succ(wv10800)), wv79) → new_intersectBy00012(wv74, wv7500, wv770, wv10800, wv79)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Zero, Pos(Zero), wv52) → new_intersectBy000118(wv47, wv4800, Zero, wv52)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00015(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00045(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00026(wv30000, wv41)
new_intersectBy000113(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00014(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00092(wv34, wv3500, wv1480, Zero, wv39) → new_intersectBy0005(wv34, Succ(wv3500), wv39)
new_intersectBy000103(wv60, wv6100, Succ(wv20400), Succ(Zero), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00055(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00052(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Zero, Pos(Zero), wv65) → new_intersectBy000106(wv60, wv6100, Zero, wv65)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00040(wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00040(wv41)
new_intersectBy00071(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00070(wv41)
new_intersectBy00012(wv74, wv7500, Succ(wv770), Zero, wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00012(wv74, wv7500, Zero, Succ(wv10800), wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Zero, Pos(Succ(wv3800)), wv39) → new_intersectBy00098(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Zero, Neg(Zero), wv39) → new_intersectBy00099(wv34, wv3500, Zero, wv39)
new_intersectBy000(wv74, Pos(Zero), Zero, wv77, Pos(Zero), wv79) → new_intersectBy0006(wv74, wv77, wv79)
new_intersectBy000100(wv74, wv7500, Zero, Succ(wv11000), wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy000100(wv74, wv7500, Succ(wv770), Zero, wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy0007(Float(Neg(Zero), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00085(wv301, wv401, wv41)
new_intersectBy00031(Succ(wv1260), wv41) → new_intersectBy00087(wv41)
new_intersectBy00081(wv306, wv41) → new_intersectBy000114(wv41)
new_intersectBy00021(wv30000, wv94, wv41) → new_intersectBy0009(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy00085(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00077(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00034(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000122(wv74, Zero, wv77, Zero, wv79) → new_intersectBy00010(wv74, wv77, wv79)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00067(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00073(wv30100000, Succ(wv2680), wv41) → new_intersectBy000109(wv30100000, wv41)
new_intersectBy00042(wv34, Neg(wv350), Succ(wv1480), Neg(wv380), wv39) → new_intersectBy0009(wv34, wv350, wv39)
new_intersectBy00072(wv47, Neg(wv480), Succ(wv2600), Pos(wv510), wv52) → new_intersectBy000104(wv47, wv480, wv52)
new_intersectBy000115(wv47, wv2600, wv52) → new_intersectBy000101(wv47, Zero, wv52)
new_intersectBy00059(wv220, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00025(wv30000, wv107, wv41) → new_intersectBy0009(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy00085(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00083(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Zero, Pos(Succ(wv3800)), wv39) → new_intersectBy00096(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy000(wv74, Pos(wv750), Succ(wv760), wv77, Neg(wv780), wv79) → new_intersectBy0001(wv74, wv750, new_primPlusNat0(wv760, wv77), wv780, wv79)
new_intersectBy00071(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00061(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00045(wv164, wv41) → new_intersectBy00088(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00065(Succ(wv2350), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00034(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00080(Succ(wv2910), wv41) → new_intersectBy000113(wv41)
new_intersectBy00035(Succ(wv1350), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00055(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00040(wv41)
new_intersectBy00034(wv30100000, Succ(wv1300), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy000108(wv60, wv6100, Succ(wv20400), Succ(wv23800), wv65) → new_intersectBy000108(wv60, wv6100, wv20400, wv23800, wv65)
new_intersectBy00055(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00047(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00024(wv30000, Succ(wv1040), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Succ(wv1480), Neg(Zero), wv39) → new_intersectBy00092(wv34, wv3500, wv1480, Zero, wv39)
new_intersectBy00069(wv259, wv41) → new_intersectBy000114(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00033(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00033(wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00016(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00088(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00085(Pos(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00063(wv41)
new_intersectBy00041(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00037(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00092(wv34, wv3500, wv1480, Succ(wv1820), wv39) → new_intersectBy00012(wv34, wv3500, wv1480, wv1820, wv39)
new_intersectBy00085(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00084(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00028(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Succ(wv2040), Pos(Zero), wv65) → new_intersectBy000103(wv60, wv6100, wv2040, Zero, wv65)
new_intersectBy0008(wv74, wv7500, Succ(wv770), Succ(Succ(wv11000)), wv79) → new_intersectBy000100(wv74, wv7500, wv770, wv11000, wv79)
new_intersectBy00049(wv30100000, Succ(wv1740), wv41) → new_intersectBy00089(wv30100000, wv41)
new_intersectBy0004(wv74, wv7500, Succ(wv770), Succ(Zero), wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy000103(wv60, wv6100, Succ(wv20400), Succ(Succ(wv23800)), wv65) → new_intersectBy000108(wv60, wv6100, wv20400, wv23800, wv65)
new_intersectBy00032(wv129, wv41) → new_intersectBy00088(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00027(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Neg(wv610), Succ(wv2040), Neg(wv640), :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Neg(wv610)), wv650, wv651)
new_intersectBy00055(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00050(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000118(wv47, wv4800, Succ(wv2960), wv52) → new_intersectBy000104(wv47, Succ(wv4800), wv52)
new_intersectBy00046(wv30100000, Succ(wv1650), wv41) → new_intersectBy00086(wv30100000, wv41)
new_intersectBy00050(Succ(wv1790), wv41) → new_intersectBy00090(wv41)
new_intersectBy00022(wv74, wv750, wv790, wv791) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy00055(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00051(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy0007(Float(Pos(Zero), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00055(wv301, wv401, wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy00022(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy00041(Neg(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy000(wv74, Neg(wv750), Zero, wv77, Pos(wv780), :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy00042(wv34, Neg(Zero), Succ(wv1480), Pos(Succ(wv3800)), wv39) → new_intersectBy0009(wv34, Zero, wv39)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00081(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00033(wv41)
new_intersectBy00011(wv74, Succ(wv7500), wv77, Succ(wv7800), wv79) → new_intersectBy0004(wv74, wv7500, wv77, new_primPlusNat0(new_primMulNat0(wv7500, wv7800), Succ(wv7800)), wv79)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00047(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00054(wv203, wv41) → new_intersectBy00091(wv41)
new_intersectBy000104(wv60, wv610, :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Neg(wv610)), wv650, wv651)
new_intersectBy0008(wv74, wv7500, Succ(wv770), Succ(Zero), wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00021(wv30000, new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00057(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0009(wv74, wv750, :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy0007(Float(Neg(Zero), wv301), Float(Pos(Zero), wv401), wv41) → new_intersectBy00071(wv301, wv401, wv41)
new_intersectBy00042(wv34, Pos(Zero), Succ(wv1480), Neg(Succ(wv3800)), wv39) → new_intersectBy0005(wv34, Zero, wv39)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00083(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00066(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00055(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00053(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Zero, Neg(Succ(wv5100)), wv52) → new_intersectBy000119(wv47, wv4800, new_primPlusNat0(new_primMulNat0(wv4800, wv5100), Succ(wv5100)), wv52)
new_intersectBy000119(wv47, wv4800, Succ(wv2980), wv52) → new_intersectBy000104(wv47, Succ(wv4800), wv52)
new_intersectBy00042(wv34, Pos(Zero), Succ(wv1480), Neg(Zero), wv39) → new_intersectBy00093(wv34, wv1480, wv39)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00033(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00062(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00031(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00078(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00013(wv74, wv750, wv790, wv791) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy00091(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00075(wv276, wv41) → new_intersectBy000111(wv41)
new_intersectBy00056(wv60, Pos(wv610), Succ(wv2040), Pos(wv640), :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Pos(wv610)), wv650, wv651)
new_intersectBy00056(wv60, Pos(Zero), Succ(wv2040), Neg(Zero), wv65) → new_intersectBy000102(wv60, wv2040, wv65)
new_intersectBy00072(wv47, Neg(Zero), Succ(wv2600), Neg(Zero), wv52) → new_intersectBy000117(wv47, wv2600, wv52)
new_intersectBy00055(Neg(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00040(wv41)
new_intersectBy00085(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00076(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy00040(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00044(Succ(wv1610), wv41) → new_intersectBy00087(wv41)
new_intersectBy000122(wv74, Succ(wv7500), wv77, Succ(wv7800), wv79) → new_intersectBy0008(wv74, wv7500, wv77, new_primPlusNat0(new_primMulNat0(wv7500, wv7800), Succ(wv7800)), wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00018(wv30000, wv41)
new_intersectBy00096(wv34, wv3500, Succ(wv1860), wv39) → new_intersectBy0005(wv34, Succ(wv3500), wv39)
new_intersectBy00061(Succ(wv2260), wv41) → new_intersectBy000110(wv41)
new_intersectBy00016(wv30000, wv30100000, Succ(wv3220), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy00084(wv315, wv41) → new_intersectBy000114(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00065(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Neg(Zero), Succ(wv2040), Pos(Zero), wv65) → new_intersectBy000105(wv60, wv2040, wv65)
new_intersectBy000(wv74, Neg(wv750), Succ(wv760), wv77, Pos(wv780), wv79) → new_intersectBy0002(wv74, wv750, new_primPlusNat0(wv760, wv77), wv780, wv79)
new_intersectBy00071(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00043(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00030(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00066(wv250, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00094(wv34, wv3500, wv1480, Succ(wv1840), wv39) → new_intersectBy000100(wv34, wv3500, wv1480, wv1840, wv39)
new_intersectBy00087(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy000111(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00050(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00060(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) → new_intersectBy0003(wv74, wv750, wv98, wv780, wv79)
new_intersectBy0008(wv74, wv7500, Zero, Succ(Succ(wv11000)), wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Succ(wv1480), Neg(Succ(wv3800)), wv39) → new_intersectBy00092(wv34, wv3500, wv1480, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00041(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00038(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00072(wv30000, wv301, Zero, wv401, wv41)
new_intersectBy00011(wv74, Zero, wv77, Zero, wv79) → new_intersectBy0006(wv74, wv77, wv79)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Pos(Succ(wv40000)), wv401), wv41) → new_intersectBy00056(wv30000, wv301, new_primPlusNat0(new_primMulNat0(wv30000, wv40000), Succ(wv40000)), wv401, wv41)
new_intersectBy000120(wv74, wv750, wv77, wv780, :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy000114(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00071(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00062(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00071(Neg(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00038(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Succ(wv1480), Pos(Zero), wv39) → new_intersectBy00094(wv34, wv3500, wv1480, Zero, wv39)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Neg(Succ(wv40000)), wv401), wv41) → new_intersectBy00072(wv30000, wv301, new_primPlusNat0(new_primMulNat0(wv30000, wv40000), Succ(wv40000)), wv401, wv41)
new_intersectBy00089(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy000(wv74, Neg(Zero), Zero, wv77, Neg(Zero), wv79) → new_intersectBy00010(wv74, wv77, wv79)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Succ(wv1480), Pos(Succ(wv3800)), wv39) → new_intersectBy00094(wv34, wv3500, wv1480, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00041(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00032(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00060(wv30100000, Succ(wv2210), wv41) → new_intersectBy000109(wv30100000, wv41)
new_intersectBy00055(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00044(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Neg(Zero), Succ(wv2040), Pos(Succ(wv6400)), wv65) → new_intersectBy000104(wv60, Zero, wv65)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00074(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00048(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00032(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00042(wv30000, wv301, Zero, wv401, wv41)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Zero, Neg(Succ(wv3800)), wv39) → new_intersectBy00099(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Zero, Pos(Zero), wv39) → new_intersectBy00098(wv34, wv3500, Zero, wv39)
new_intersectBy00041(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00040(wv41)
new_intersectBy000103(wv60, wv6100, wv2040, Zero, wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy000(wv74, Neg(Succ(wv7500)), Zero, wv77, Neg(Succ(wv7800)), wv79) → new_intersectBy0008(wv74, wv7500, wv77, new_primPlusNat0(new_primMulNat0(wv7500, wv7800), Succ(wv7800)), wv79)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Zero, Neg(Succ(wv6400)), wv65) → new_intersectBy000107(wv60, wv6100, new_primPlusNat0(new_primMulNat0(wv6100, wv6400), Succ(wv6400)), wv65)
new_intersectBy000(wv74, Pos(Zero), Zero, wv77, Pos(Succ(wv7800)), wv79) → new_intersectBy0005(wv74, Zero, wv79)
new_intersectBy00010(wv74, wv77, wv79) → new_intersectBy0009(wv74, Zero, wv79)
new_intersectBy000(wv74, Neg(Succ(wv7500)), Zero, wv77, Neg(Zero), wv79) → new_intersectBy0008(wv74, wv7500, wv77, Zero, wv79)
new_intersectBy00055(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00048(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00043(wv30100000, Succ(wv1560), wv41) → new_intersectBy00086(wv30100000, wv41)
new_intersectBy00036(wv138, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00058(Succ(wv2170), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00063(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00053(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00029(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00035(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000106(wv60, wv6100, Succ(wv2400), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00041(Pos(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy00028(Succ(wv1170), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00068(Succ(wv2560), wv41) → new_intersectBy000113(wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00024(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00066(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00097(wv34, wv3500, Succ(wv1880), wv39) → new_intersectBy0005(wv34, Succ(wv3500), wv39)
new_intersectBy00076(wv30100000, Succ(wv2770), wv41) → new_intersectBy000109(wv30100000, wv41)
new_intersectBy000(wv74, Pos(wv750), Zero, wv77, Neg(wv780), :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy000108(wv60, wv6100, Succ(wv20400), Zero, wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy000108(wv60, wv6100, Zero, Succ(wv23800), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00085(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00073(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00080(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00084(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00047(Succ(wv1700), wv41) → new_intersectBy00087(wv41)
new_intersectBy000(wv74, Pos(Succ(wv7500)), Zero, wv77, Pos(Succ(wv7800)), wv79) → new_intersectBy0004(wv74, wv7500, wv77, new_primPlusNat0(new_primMulNat0(wv7500, wv7800), Succ(wv7800)), wv79)
new_intersectBy00042(wv34, Neg(Zero), Succ(wv1480), Pos(Zero), wv39) → new_intersectBy00095(wv34, wv1480, wv39)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00040(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00077(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000101(wv60, wv610, :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Pos(wv610)), wv650, wv651)
new_intersectBy00038(Succ(wv1440), wv41) → new_intersectBy00090(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00058(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00056(wv60, Pos(Zero), Succ(wv2040), Neg(Succ(wv6400)), wv65) → new_intersectBy000101(wv60, Zero, wv65)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Pos(Zero), wv401), wv41) → new_intersectBy00056(wv30000, wv301, Zero, wv401, wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00082(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00035(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00014(wv30000, wv30100000, Succ(wv3160), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy00085(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00082(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00075(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00085(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00075(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00093(wv34, wv1480, wv39) → new_intersectBy0005(wv34, Zero, wv39)
new_intersectBy000(wv74, Neg(Zero), Zero, wv77, Neg(Succ(wv7800)), wv79) → new_intersectBy0009(wv74, Zero, wv79)
new_intersectBy00072(wv47, Pos(Zero), Succ(wv2600), Pos(Succ(wv5100)), wv52) → new_intersectBy000101(wv47, Zero, wv52)
new_intersectBy000122(wv74, Zero, wv77, Succ(wv7800), wv79) → new_intersectBy0009(wv74, Zero, wv79)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00045(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00079(wv30100000, Succ(wv2860), wv41) → new_intersectBy000112(wv30100000, wv41)
new_intersectBy00086(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs with 22 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
QDP
                                  ↳ UsableRulesProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) → new_intersectBy0003(wv74, wv750, wv98, wv780, wv79)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                  ↳ UsableRulesProof
QDP
                                      ↳ QReductionProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) → new_intersectBy0003(wv74, wv750, wv98, wv780, wv79)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
QDP
                                          ↳ NonTerminationProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) → new_intersectBy0003(wv74, wv750, wv98, wv780, wv79)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) → new_intersectBy0003(wv74, wv750, wv98, wv780, wv79)

The TRS R consists of the following rules:none


s = new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) evaluates to t =new_intersectBy0003(wv74, wv750, wv98, wv780, wv79)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_intersectBy0003(wv74, wv750, wv98, wv780, wv79) to new_intersectBy0003(wv74, wv750, wv98, wv780, wv79).





↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
QDP
                                  ↳ UsableRulesProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) → new_intersectBy0001(wv74, wv750, wv96, wv780, wv79)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
QDP
                                      ↳ QReductionProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) → new_intersectBy0001(wv74, wv750, wv96, wv780, wv79)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
QDP
                                          ↳ NonTerminationProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) → new_intersectBy0001(wv74, wv750, wv96, wv780, wv79)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) → new_intersectBy0001(wv74, wv750, wv96, wv780, wv79)

The TRS R consists of the following rules:none


s = new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) evaluates to t =new_intersectBy0001(wv74, wv750, wv96, wv780, wv79)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_intersectBy0001(wv74, wv750, wv96, wv780, wv79) to new_intersectBy0001(wv74, wv750, wv96, wv780, wv79).





↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
QDP
                                  ↳ UsableRulesProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) → new_intersectBy0002(wv74, wv750, wv97, wv780, wv79)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
QDP
                                      ↳ QReductionProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) → new_intersectBy0002(wv74, wv750, wv97, wv780, wv79)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
QDP
                                          ↳ NonTerminationProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) → new_intersectBy0002(wv74, wv750, wv97, wv780, wv79)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) → new_intersectBy0002(wv74, wv750, wv97, wv780, wv79)

The TRS R consists of the following rules:none


s = new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) evaluates to t =new_intersectBy0002(wv74, wv750, wv97, wv780, wv79)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_intersectBy0002(wv74, wv750, wv97, wv780, wv79) to new_intersectBy0002(wv74, wv750, wv97, wv780, wv79).





↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
QDP
                                  ↳ QDPSizeChangeProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy000103(wv60, wv6100, wv2040, Zero, wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00056(wv60, Neg(Zero), Succ(wv2040), Pos(Zero), wv65) → new_intersectBy000105(wv60, wv2040, wv65)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Zero, Neg(Succ(wv6400)), wv65) → new_intersectBy000107(wv60, wv6100, new_primPlusNat0(new_primMulNat0(wv6100, wv6400), Succ(wv6400)), wv65)
new_intersectBy000105(wv60, wv2040, wv65) → new_intersectBy000104(wv60, Zero, wv65)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Succ(wv2040), Pos(Succ(wv6400)), wv65) → new_intersectBy000103(wv60, wv6100, wv2040, new_primPlusNat0(new_primMulNat0(wv6100, wv6400), Succ(wv6400)), wv65)
new_intersectBy000106(wv60, wv6100, Succ(wv2400), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Zero, Pos(Succ(wv5100)), wv52) → new_intersectBy000118(wv47, wv4800, new_primPlusNat0(new_primMulNat0(wv4800, wv5100), Succ(wv5100)), wv52)
new_intersectBy000104(wv60, wv610, :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Neg(wv610)), wv650, wv651)
new_intersectBy000108(wv60, wv6100, Succ(wv20400), Succ(wv23800), wv65) → new_intersectBy000108(wv60, wv6100, wv20400, wv23800, wv65)
new_intersectBy000108(wv60, wv6100, Succ(wv20400), Zero, wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy000108(wv60, wv6100, Zero, Succ(wv23800), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00072(wv47, Pos(Zero), Succ(wv2600), Pos(Zero), wv52) → new_intersectBy000115(wv47, wv2600, wv52)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Pos(Succ(wv40000)), wv401), wv41) → new_intersectBy00056(wv30000, wv301, new_primPlusNat0(new_primMulNat0(wv30000, wv40000), Succ(wv40000)), wv401, wv41)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00072(wv30000, wv301, Zero, wv401, wv41)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Zero, Neg(Succ(wv5100)), wv52) → new_intersectBy000119(wv47, wv4800, new_primPlusNat0(new_primMulNat0(wv4800, wv5100), Succ(wv5100)), wv52)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Succ(wv2600), Neg(Succ(wv5100)), wv52) → new_intersectBy000116(wv47, wv4800, wv2600, new_primPlusNat0(new_primMulNat0(wv4800, wv5100), Succ(wv5100)), wv52)
new_intersectBy000119(wv47, wv4800, Succ(wv2980), wv52) → new_intersectBy000104(wv47, Succ(wv4800), wv52)
new_intersectBy00072(wv47, Neg(Zero), Succ(wv2600), Neg(Succ(wv5100)), wv52) → new_intersectBy000104(wv47, Zero, wv52)
new_intersectBy000103(wv60, wv6100, Succ(wv20400), Succ(Zero), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Succ(wv2040), Pos(Zero), wv65) → new_intersectBy000103(wv60, wv6100, wv2040, Zero, wv65)
new_intersectBy00072(wv47, Pos(wv480), Succ(wv2600), Neg(wv510), wv52) → new_intersectBy000101(wv47, wv480, wv52)
new_intersectBy000101(wv60, wv610, :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Pos(wv610)), wv650, wv651)
new_intersectBy00056(wv60, Pos(Zero), Succ(wv2040), Neg(Succ(wv6400)), wv65) → new_intersectBy000101(wv60, Zero, wv65)
new_intersectBy000103(wv60, wv6100, Succ(wv20400), Succ(Succ(wv23800)), wv65) → new_intersectBy000108(wv60, wv6100, wv20400, wv23800, wv65)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Neg(Succ(wv40000)), wv401), wv41) → new_intersectBy00072(wv30000, wv301, new_primPlusNat0(new_primMulNat0(wv30000, wv40000), Succ(wv40000)), wv401, wv41)
new_intersectBy0007(Float(Neg(Succ(wv30000)), wv301), Float(Pos(Zero), wv401), wv41) → new_intersectBy00056(wv30000, wv301, Zero, wv401, wv41)
new_intersectBy000116(wv47, wv4800, wv2600, Succ(wv2940), wv52) → new_intersectBy000108(wv47, wv4800, wv2600, wv2940, wv52)
new_intersectBy00056(wv60, Pos(wv610), Succ(wv2040), Pos(wv640), :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Pos(wv610)), wv650, wv651)
new_intersectBy00056(wv60, Pos(Zero), Succ(wv2040), Neg(Zero), wv65) → new_intersectBy000102(wv60, wv2040, wv65)
new_intersectBy00072(wv47, Neg(Zero), Succ(wv2600), Neg(Zero), wv52) → new_intersectBy000117(wv47, wv2600, wv52)
new_intersectBy00056(wv60, Neg(wv610), Succ(wv2040), Neg(wv640), :(wv650, wv651)) → new_intersectBy0007(Float(Neg(Succ(wv60)), Neg(wv610)), wv650, wv651)
new_intersectBy00056(wv60, Neg(Zero), Succ(wv2040), Pos(Succ(wv6400)), wv65) → new_intersectBy000104(wv60, Zero, wv65)
new_intersectBy000117(wv47, wv2600, wv52) → new_intersectBy000104(wv47, Zero, wv52)
new_intersectBy000116(wv47, wv4800, wv2600, Zero, wv52) → new_intersectBy000104(wv47, Succ(wv4800), wv52)
new_intersectBy00072(wv47, Pos(Zero), Succ(wv2600), Pos(Succ(wv5100)), wv52) → new_intersectBy000101(wv47, Zero, wv52)
new_intersectBy000118(wv47, wv4800, Succ(wv2960), wv52) → new_intersectBy000104(wv47, Succ(wv4800), wv52)
new_intersectBy00072(wv47, Neg(Succ(wv4800)), Succ(wv2600), Neg(Zero), wv52) → new_intersectBy000116(wv47, wv4800, wv2600, Zero, wv52)
new_intersectBy00072(wv47, Neg(wv480), Succ(wv2600), Pos(wv510), wv52) → new_intersectBy000104(wv47, wv480, wv52)
new_intersectBy000103(wv60, wv6100, Zero, Succ(Succ(wv23800)), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy000115(wv47, wv2600, wv52) → new_intersectBy000101(wv47, Zero, wv52)
new_intersectBy000107(wv60, wv6100, Succ(wv2420), wv65) → new_intersectBy000104(wv60, Succ(wv6100), wv65)
new_intersectBy000102(wv60, wv2040, wv65) → new_intersectBy000101(wv60, Zero, wv65)
new_intersectBy00056(wv60, Neg(Succ(wv6100)), Zero, Pos(Succ(wv6400)), wv65) → new_intersectBy000106(wv60, wv6100, new_primPlusNat0(new_primMulNat0(wv6100, wv6400), Succ(wv6400)), wv65)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
QDP
                                  ↳ QDPSizeChangeProof
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy00085(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00083(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00085(Neg(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00070(wv41)
new_intersectBy00078(wv285, wv41) → new_intersectBy000111(wv41)
new_intersectBy00071(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00061(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00065(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy00065(Succ(wv2350), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00080(Succ(wv2910), wv41) → new_intersectBy000113(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00069(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00073(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00085(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00078(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00069(wv259, wv41) → new_intersectBy000114(wv41)
new_intersectBy00067(wv30100000, Succ(wv2510), wv41) → new_intersectBy000112(wv30100000, wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00068(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00085(Pos(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00063(wv41)
new_intersectBy00085(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00084(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00083(Succ(wv3120), wv41) → new_intersectBy000113(wv41)
new_intersectBy00071(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00064(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00060(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00085(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00079(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00059(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00059(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00057(wv30100000, Succ(wv2120), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00064(wv30100000, Succ(wv2300), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00070(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00076(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00081(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00071(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00067(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00057(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), wv301), Float(Pos(Zero), wv401), wv41) → new_intersectBy00071(wv301, wv401, wv41)
new_intersectBy000109(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00071(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00057(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00061(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00083(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00066(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00062(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00078(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00071(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00068(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000110(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00075(wv276, wv41) → new_intersectBy000111(wv41)
new_intersectBy00062(wv229, wv41) → new_intersectBy000111(wv41)
new_intersectBy00085(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00076(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Pos(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy00061(Succ(wv2260), wv41) → new_intersectBy000110(wv41)
new_intersectBy00084(wv315, wv41) → new_intersectBy000114(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00065(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00063(wv41)
new_intersectBy00066(wv250, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00085(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00070(wv41)
new_intersectBy00085(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00080(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00063(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00070(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00070(wv41)
new_intersectBy00082(wv30100000, Succ(wv3070), wv41) → new_intersectBy000112(wv30100000, wv41)
new_intersectBy000111(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00071(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00060(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000114(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00071(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00062(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00071(Neg(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00077(Succ(wv2820), wv41) → new_intersectBy000110(wv41)
new_intersectBy00070(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00085(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00081(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00074(Succ(wv2730), wv41) → new_intersectBy000110(wv41)
new_intersectBy00060(wv30100000, Succ(wv2210), wv41) → new_intersectBy000109(wv30100000, wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00074(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00064(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00079(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000112(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00085(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00063(wv41)
new_intersectBy00071(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00069(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00063(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy00058(Succ(wv2170), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00071(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00058(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00085(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00074(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00068(Succ(wv2560), wv41) → new_intersectBy000113(wv41)
new_intersectBy00071(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00066(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00076(wv30100000, Succ(wv2770), wv41) → new_intersectBy000109(wv30100000, wv41)
new_intersectBy000113(:(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00085(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00073(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00080(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00084(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00077(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00058(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00071(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00070(wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00082(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00085(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00082(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00075(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00085(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00075(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Neg(Zero), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00085(wv301, wv401, wv41)
new_intersectBy00081(wv306, wv41) → new_intersectBy000114(wv41)
new_intersectBy00085(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00077(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Neg(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00067(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00073(wv30100000, Succ(wv2680), wv41) → new_intersectBy000109(wv30100000, wv41)
new_intersectBy00079(wv30100000, Succ(wv2860), wv41) → new_intersectBy000112(wv30100000, wv41)
new_intersectBy00059(wv220, :(wv410, wv411)) → new_intersectBy0007(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
QDP
                                  ↳ QDPSizeChangeProof
                                ↳ QDP
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy00048(wv173, wv41) → new_intersectBy00088(wv41)
new_intersectBy00052(wv30100000, Succ(wv1950), wv41) → new_intersectBy00089(wv30100000, wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00046(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00045(wv164, wv41) → new_intersectBy00088(wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00034(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00037(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00035(Succ(wv1350), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00055(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00040(wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00027(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00034(wv30100000, Succ(wv1300), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00037(wv30100000, Succ(wv1390), wv41) → new_intersectBy00089(wv30100000, wv41)
new_intersectBy00055(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00046(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00054(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00055(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00047(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00030(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00033(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00033(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00033(wv41)
new_intersectBy00041(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00029(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00039(wv147, wv41) → new_intersectBy00091(wv41)
new_intersectBy00088(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00041(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00037(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00028(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00049(wv30100000, Succ(wv1740), wv41) → new_intersectBy00089(wv30100000, wv41)
new_intersectBy00032(wv129, wv41) → new_intersectBy00088(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00031(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00027(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00050(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00046(wv30100000, Succ(wv1650), wv41) → new_intersectBy00086(wv30100000, wv41)
new_intersectBy00050(Succ(wv1790), wv41) → new_intersectBy00090(wv41)
new_intersectBy00055(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00051(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00055(wv301, wv401, wv41)
new_intersectBy00030(wv30100000, Succ(wv1210), wv41) → new_intersectBy00086(wv30100000, wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00036(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Neg(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy00055(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00043(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00033(wv41)
new_intersectBy00054(wv203, wv41) → new_intersectBy00091(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00047(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Pos(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00033(wv41)
new_intersectBy00055(Pos(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00033(wv41)
new_intersectBy00027(wv30100000, Succ(wv1120), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00049(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00053(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00033(wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00031(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00090(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00091(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy00055(Neg(Succ(Zero)), Pos(Succ(wv40100)), wv41) → new_intersectBy00040(wv41)
new_intersectBy00040(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), wv301), Float(Pos(Zero), wv401), wv41) → new_intersectBy00041(wv301, wv401, wv41)
new_intersectBy00041(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00039(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00044(Succ(wv1610), wv41) → new_intersectBy00087(wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00043(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00030(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00028(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00087(:(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00050(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00039(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Neg(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00036(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Neg(Succ(Succ(Succ(Zero)))), Neg(Succ(wv40100)), wv41) → new_intersectBy00038(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00038(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00055(Neg(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00054(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00089(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)
new_intersectBy00055(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00049(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00032(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00055(Pos(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00044(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00044(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00051(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00048(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00032(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00051(wv194, wv41) → new_intersectBy00091(wv41)
new_intersectBy00029(wv120, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00052(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Neg(Succ(Zero)), Neg(Succ(wv40100)), wv41) → new_intersectBy00040(wv41)
new_intersectBy00053(Succ(wv2000), wv41) → new_intersectBy00090(wv41)
new_intersectBy00043(wv30100000, Succ(wv1560), wv41) → new_intersectBy00086(wv30100000, wv41)
new_intersectBy00055(Pos(Succ(Succ(Zero))), Neg(Succ(wv40100)), wv41) → new_intersectBy00048(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00036(wv138, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wv410, wv411)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00053(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00029(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00041(Neg(Succ(Succ(Succ(Zero)))), Pos(Succ(wv40100)), wv41) → new_intersectBy00035(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00041(Pos(Succ(Zero)), Pos(Succ(wv40100)), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Zero))), wv410, wv411)
new_intersectBy00028(Succ(wv1170), :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Zero))))), wv410, wv411)
new_intersectBy00055(Pos(Succ(Succ(Zero))), Pos(Succ(wv40100)), wv41) → new_intersectBy00045(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00047(Succ(wv1700), wv41) → new_intersectBy00087(wv41)
new_intersectBy00055(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Neg(Succ(wv40100)), wv41) → new_intersectBy00052(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00040(wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(wv40000)), Neg(Succ(wv40100))), wv41) → new_intersectBy00040(wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00040(wv41)
new_intersectBy00038(Succ(wv1440), wv41) → new_intersectBy00090(wv41)
new_intersectBy0007(Float(Pos(Zero), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00035(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00031(Succ(wv1260), wv41) → new_intersectBy00087(wv41)
new_intersectBy00041(Neg(Succ(Succ(Succ(Succ(wv30100000))))), Pos(Succ(wv40100)), wv41) → new_intersectBy00034(wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(wv40000)), Pos(Succ(wv40100))), wv41) → new_intersectBy00045(new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00086(wv30100000, :(wv410, wv411)) → new_intersectBy0007(Float(Pos(Zero), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), wv410, wv411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
QDP
                                  ↳ UsableRulesProof
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) → new_intersectBy0000(wv74, wv750, wv95, wv780, wv79)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
QDP
                                      ↳ QReductionProof
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) → new_intersectBy0000(wv74, wv750, wv95, wv780, wv79)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
QDP
                                          ↳ NonTerminationProof
                                ↳ QDP
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) → new_intersectBy0000(wv74, wv750, wv95, wv780, wv79)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) → new_intersectBy0000(wv74, wv750, wv95, wv780, wv79)

The TRS R consists of the following rules:none


s = new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) evaluates to t =new_intersectBy0000(wv74, wv750, wv95, wv780, wv79)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_intersectBy0000(wv74, wv750, wv95, wv780, wv79) to new_intersectBy0000(wv74, wv750, wv95, wv780, wv79).





↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
                                ↳ QDP
QDP
                                  ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_intersectBy00016(wv30000, wv30100000, Succ(wv3220), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy0008(wv74, wv7500, wv77, Zero, wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00023(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Zero, Pos(Succ(wv3800)), wv39) → new_intersectBy00096(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00023(wv30000, wv30100000, Succ(wv990), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy00098(wv34, wv3500, Succ(wv1900), wv39) → new_intersectBy0009(wv34, Succ(wv3500), wv39)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Zero, Neg(Succ(wv3800)), wv39) → new_intersectBy00097(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00012(wv74, wv7500, Succ(wv770), Succ(wv10800), wv79) → new_intersectBy00012(wv74, wv7500, wv770, wv10800, wv79)
new_intersectBy00018(wv30000, :(wv410, wv411)) → new_intersectBy00013(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy00094(wv34, wv3500, wv1480, Succ(wv1840), wv39) → new_intersectBy000100(wv34, wv3500, wv1480, wv1840, wv39)
new_intersectBy0008(wv74, wv7500, Zero, Succ(Succ(wv11000)), wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Succ(wv1480), Neg(Succ(wv3800)), wv39) → new_intersectBy00092(wv34, wv3500, wv1480, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00024(wv30000, Succ(wv1040), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy00042(wv34, Pos(Succ(wv3500)), Succ(wv1480), Neg(Zero), wv39) → new_intersectBy00092(wv34, wv3500, wv1480, Zero, wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), wv301), Float(Neg(Succ(wv40000)), wv401), wv41) → new_intersectBy00042(wv30000, wv301, new_primPlusNat0(new_primMulNat0(wv30000, wv40000), Succ(wv40000)), wv401, wv41)
new_intersectBy0005(wv74, wv750, :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy000100(wv74, wv7500, Succ(wv770), Succ(wv11000), wv79) → new_intersectBy000100(wv74, wv7500, wv770, wv11000, wv79)
new_intersectBy0004(wv74, wv7500, Zero, Succ(Succ(wv10800)), wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00016(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00092(wv34, wv3500, wv1480, Succ(wv1820), wv39) → new_intersectBy00012(wv34, wv3500, wv1480, wv1820, wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00017(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0008(wv74, wv7500, Succ(wv770), Succ(Succ(wv11000)), wv79) → new_intersectBy000100(wv74, wv7500, wv770, wv11000, wv79)
new_intersectBy00015(wv30000, Succ(wv3200), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy0004(wv74, wv7500, Succ(wv770), Succ(Zero), wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Succ(wv1480), Pos(Zero), wv39) → new_intersectBy00094(wv34, wv3500, wv1480, Zero, wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy00013(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy000(wv74, Neg(Zero), Zero, wv77, Neg(Zero), wv79) → new_intersectBy00010(wv74, wv77, wv79)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Succ(wv1480), Pos(Succ(wv3800)), wv39) → new_intersectBy00094(wv34, wv3500, wv1480, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00019(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00025(wv30000, new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy00094(wv34, wv3500, wv1480, Zero, wv39) → new_intersectBy0009(wv34, Succ(wv3500), wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), wv301), Float(Neg(Zero), wv401), wv41) → new_intersectBy00042(wv30000, wv301, Zero, wv401, wv41)
new_intersectBy0004(wv74, wv7500, wv77, Zero, wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00017(wv30000, Succ(wv830), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Zero, Neg(Succ(wv3800)), wv39) → new_intersectBy00099(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy00022(wv74, wv750, wv790, wv791) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy000(wv74, Neg(Succ(wv7500)), Zero, wv77, Neg(Succ(wv7800)), wv79) → new_intersectBy0008(wv74, wv7500, wv77, new_primPlusNat0(new_primMulNat0(wv7500, wv7800), Succ(wv7800)), wv79)
new_intersectBy000(wv74, Pos(Succ(wv7500)), Zero, wv77, Pos(Zero), wv79) → new_intersectBy0004(wv74, wv7500, wv77, Zero, wv79)
new_intersectBy0006(wv74, wv77, wv79) → new_intersectBy0005(wv74, Zero, wv79)
new_intersectBy000(wv74, Pos(Zero), Zero, wv77, Pos(Succ(wv7800)), wv79) → new_intersectBy0005(wv74, Zero, wv79)
new_intersectBy00010(wv74, wv77, wv79) → new_intersectBy0009(wv74, Zero, wv79)
new_intersectBy00099(wv34, wv3500, Succ(wv1920), wv39) → new_intersectBy0009(wv34, Succ(wv3500), wv39)
new_intersectBy000(wv74, Neg(Succ(wv7500)), Zero, wv77, Neg(Zero), wv79) → new_intersectBy0008(wv74, wv7500, wv77, Zero, wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(wv40100))), :(wv410, wv411)) → new_intersectBy00022(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy0004(wv74, wv7500, Succ(wv770), Succ(Succ(wv10800)), wv79) → new_intersectBy00012(wv74, wv7500, wv770, wv10800, wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00020(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy000(wv74, Neg(wv750), Zero, wv77, Pos(wv780), :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy00042(wv34, Pos(wv350), Succ(wv1480), Pos(wv380), wv39) → new_intersectBy0005(wv34, wv350, wv39)
new_intersectBy00042(wv34, Neg(Zero), Succ(wv1480), Pos(Succ(wv3800)), wv39) → new_intersectBy0009(wv34, Zero, wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00015(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy0008(wv74, wv7500, Succ(wv770), Succ(Zero), wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Succ(Zero))))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00024(wv30000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(Zero, Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00097(wv34, wv3500, Succ(wv1880), wv39) → new_intersectBy0005(wv34, Succ(wv3500), wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00021(wv30000, new_primPlusNat0(wv40100, wv40100), wv41)
new_intersectBy0009(wv74, wv750, :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Neg(wv750)), wv790, wv791)
new_intersectBy000(wv74, Pos(wv750), Zero, wv77, Neg(wv780), :(wv790, wv791)) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00026(wv30000, wv41)
new_intersectBy00042(wv34, Pos(Zero), Succ(wv1480), Neg(Succ(wv3800)), wv39) → new_intersectBy0005(wv34, Zero, wv39)
new_intersectBy00095(wv34, wv1480, wv39) → new_intersectBy0009(wv34, Zero, wv39)
new_intersectBy00020(wv30000, Succ(wv910), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Zero))), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), wv301), Float(Pos(Succ(wv40000)), wv401), wv41) → new_intersectBy000(wv30000, wv301, new_primMulNat0(wv30000, wv40000), wv40000, wv401, wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Succ(Succ(wv30100000)))))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy00014(wv30000, wv30100000, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wv30100000, wv40100), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), Succ(wv40100)), wv41)
new_intersectBy00019(wv30000, wv30100000, Succ(wv860), wv41) → new_intersectBy0009(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy00092(wv34, wv3500, wv1480, Zero, wv39) → new_intersectBy0005(wv34, Succ(wv3500), wv39)
new_intersectBy00042(wv34, Pos(Zero), Succ(wv1480), Neg(Zero), wv39) → new_intersectBy00093(wv34, wv1480, wv39)
new_intersectBy000(wv74, Pos(Succ(wv7500)), Zero, wv77, Pos(Succ(wv7800)), wv79) → new_intersectBy0004(wv74, wv7500, wv77, new_primPlusNat0(new_primMulNat0(wv7500, wv7800), Succ(wv7800)), wv79)
new_intersectBy00026(wv30000, :(wv410, wv411)) → new_intersectBy00022(wv30000, Succ(Zero), wv410, wv411)
new_intersectBy00042(wv34, Neg(Zero), Succ(wv1480), Pos(Zero), wv39) → new_intersectBy00095(wv34, wv1480, wv39)
new_intersectBy00013(wv74, wv750, wv790, wv791) → new_intersectBy0007(Float(Pos(Succ(wv74)), Pos(wv750)), wv790, wv791)
new_intersectBy00012(wv74, wv7500, Succ(wv770), Zero, wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00012(wv74, wv7500, Zero, Succ(wv10800), wv79) → new_intersectBy0005(wv74, Succ(wv7500), wv79)
new_intersectBy00042(wv34, Neg(Succ(wv3500)), Zero, Pos(Succ(wv3800)), wv39) → new_intersectBy00098(wv34, wv3500, new_primPlusNat0(new_primMulNat0(wv3500, wv3800), Succ(wv3800)), wv39)
new_intersectBy000(wv74, Pos(Zero), Zero, wv77, Pos(Zero), wv79) → new_intersectBy0006(wv74, wv77, wv79)
new_intersectBy00014(wv30000, wv30100000, Succ(wv3160), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Succ(Succ(wv30100000)))), wv41)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(wv40100))), wv41) → new_intersectBy0005(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy000100(wv74, wv7500, Zero, Succ(wv11000), wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy000100(wv74, wv7500, Succ(wv770), Zero, wv79) → new_intersectBy0009(wv74, Succ(wv7500), wv79)
new_intersectBy00093(wv34, wv1480, wv39) → new_intersectBy0005(wv34, Zero, wv39)
new_intersectBy000(wv74, Neg(Zero), Zero, wv77, Neg(Succ(wv7800)), wv79) → new_intersectBy0009(wv74, Zero, wv79)
new_intersectBy00021(wv30000, wv94, wv41) → new_intersectBy0009(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy00042(wv34, Neg(wv350), Succ(wv1480), Neg(wv380), wv39) → new_intersectBy0009(wv34, wv350, wv39)
new_intersectBy0007(Float(Pos(Succ(wv30000)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(wv40100))), wv41) → new_intersectBy00018(wv30000, wv41)
new_intersectBy00025(wv30000, wv107, wv41) → new_intersectBy0009(wv30000, Succ(Succ(Zero)), wv41)
new_intersectBy00096(wv34, wv3500, Succ(wv1860), wv39) → new_intersectBy0005(wv34, Succ(wv3500), wv39)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wv40000) → Succ(wv40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wv820), wv40000) → Succ(Succ(new_primPlusNat0(wv820, wv40000)))
new_primMulNat0(Zero, wv40000) → Zero
new_primPlusNat0(Succ(wv8200), Zero) → Succ(wv8200)
new_primPlusNat0(Zero, Succ(wv400000)) → Succ(wv400000)
new_primPlusNat0(Succ(wv8200), Succ(wv400000)) → Succ(Succ(new_primPlusNat0(wv8200, wv400000)))
new_primMulNat0(Succ(wv300000), wv40000) → new_primPlusNat1(new_primMulNat0(wv300000, wv40000), wv40000)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
new_primMulNat0(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(wv200, wv201), wv21, ba) → new_psPs(wv201, wv21, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_foldr0(wv4, :(wv30, wv31)) → new_foldr0(wv4, wv31)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:


Haskell To QDPs